M1, M2:MsgA. M1  M2  (l:IdLnk, tg:Id. M1.dout(l,tg)  M2.dout(l,tg)) 

latex

Definitions	t  T, x:A. B(x), rcv(l,tg), KindDeq, Knd, P  Q, P & Q, A & B, Valtype(da;k), MsgA, M1  M2, M.dout(l,tg), IdLnk, Id
Lemmas	Id wf, IdLnk wf, ma-sub wf, msga wf, subtype-fpf-cap-void, Knd wf, Kind-deq wf, rcv wf